Writing formal specifications for distributed systems is difficult. Evensimple consistency requirements often turn out to be unrealizable because ofthe complicated information flow in the distributed system: not all informationis available in every component, and information transmitted from othercomponents may arrive with a delay or not at all, especially in the presence offaults. The problem of checking the distributed realizability of a temporalspecification is, in general, undecidable. Semi-algorithms for synthesis, suchas bounded synthesis, are only useful in the positive case, where theyconstruct an implementation for a realizable specification, but not in thenegative case: if the specification is unrealizable, the search for theimplementation never terminates. In this paper, we introduce counterexamples todistributed realizability and present a method for the detection of suchcounterexamples for specifications given in linear-time temporal logic (LTL). Acounterexample consists of a set of paths, each representing a differentsequence of inputs from the environment, such that, no matter how thecomponents are implemented, the specification is violated on at least one ofthese paths. We present a method for finding such counterexamples both for theclassic distributed realizability problem and for the fault-tolerantrealizability problem. Our method considers, incrementally, larger and largersets of paths until a counterexample is found. For safety specifications inweakly ordered architectures we obtain a decision procedure, whilecounterexamples for full LTL and arbitrary architectures may consist ofinfinitely many paths. Experimental results, obtained with a QBF-basedprototype implementation, show that our method finds simple errors veryquickly, and even problems with high combinatorial complexity, like theByzantine Generals' Problem, are tractable.
展开▼
